Termination of the given ITRSProblem could successfully be proven:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
msort(e) → nil
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
msort(ins(x, ys)) → if_3(min(x, ys), x, ys)
if_3(pair(m, zs), x, ys) → cons(m, msort(zs))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
msort(e) → nil
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
msort(ins(x, ys)) → if_3(min(x, ys), x, ys)
if_3(pair(m, zs), x, ys) → cons(m, msort(zs))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph contains the following rules and edges:

(0): IF_1(pair(m[0], zh[0]), x[0], y[0], zs[0]) → COND_IF_1(>@z(m[0], x[0]), m[0], zh[0], x[0], y[0], zs[0])
(1): IF_2(pair(m[1], zh[1]), x[1], y[1], zs[1]) → COND_IF_2(>=@z(x[1], m[1]), m[1], zh[1], x[1], y[1], zs[1])
(2): MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])
(3): IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3])
(4): MIN(x[4], ins(y[4], zs[4])) → IF_1(min(y[4], zs[4]), x[4], y[4], zs[4])
(5): MSORT(ins(x[5], ys[5])) → MIN(x[5], ys[5])
(6): MIN(x[6], ins(y[6], zs[6])) → IF_2(min(y[6], zs[6]), x[6], y[6], zs[6])
(7): MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

(2) -> (3), if ((x[2] →* x[3])∧(ys[2] →* ys[3])∧(min(x[2], ys[2]) →* pair(m[3], zs[3])))


(3) -> (2), if ((zs[3] →* ins(x[2], ys[2])))


(3) -> (5), if ((zs[3] →* ins(x[5], ys[5])))


(4) -> (0), if ((zs[4] →* zs[0])∧(x[4] →* x[0])∧(y[4] →* y[0])∧(min(y[4], zs[4]) →* pair(m[0], zh[0])))


(5) -> (4), if ((ys[5] →* ins(y[4], zs[4]))∧(x[5] →* x[4]))


(5) -> (6), if ((ys[5] →* ins(y[6], zs[6]))∧(x[5] →* x[6]))


(5) -> (7), if ((ys[5] →* ins(y[7], zs[7]))∧(x[5] →* x[7]))


(6) -> (1), if ((zs[6] →* zs[1])∧(x[6] →* x[1])∧(y[6] →* y[1])∧(min(y[6], zs[6]) →* pair(m[1], zh[1])))


(7) -> (4), if ((zs[7] →* ins(y[4], zs[4]))∧(y[7] →* x[4]))


(7) -> (6), if ((zs[7] →* ins(y[6], zs[6]))∧(y[7] →* x[6]))


(7) -> (7), if ((zs[7] →* ins(y[7]a, zs[7]a))∧(y[7] →* x[7]a))



The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph contains the following rules and edges:

(0): IF_1(pair(m[0], zh[0]), x[0], y[0], zs[0]) → COND_IF_1(>@z(m[0], x[0]), m[0], zh[0], x[0], y[0], zs[0])
(1): IF_2(pair(m[1], zh[1]), x[1], y[1], zs[1]) → COND_IF_2(>=@z(x[1], m[1]), m[1], zh[1], x[1], y[1], zs[1])
(2): MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])
(3): IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3])
(4): MIN(x[4], ins(y[4], zs[4])) → IF_1(min(y[4], zs[4]), x[4], y[4], zs[4])
(5): MSORT(ins(x[5], ys[5])) → MIN(x[5], ys[5])
(6): MIN(x[6], ins(y[6], zs[6])) → IF_2(min(y[6], zs[6]), x[6], y[6], zs[6])
(7): MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

(2) -> (3), if ((x[2] →* x[3])∧(ys[2] →* ys[3])∧(min(x[2], ys[2]) →* pair(m[3], zs[3])))


(3) -> (2), if ((zs[3] →* ins(x[2], ys[2])))


(3) -> (5), if ((zs[3] →* ins(x[5], ys[5])))


(4) -> (0), if ((zs[4] →* zs[0])∧(x[4] →* x[0])∧(y[4] →* y[0])∧(min(y[4], zs[4]) →* pair(m[0], zh[0])))


(5) -> (4), if ((ys[5] →* ins(y[4], zs[4]))∧(x[5] →* x[4]))


(5) -> (6), if ((ys[5] →* ins(y[6], zs[6]))∧(x[5] →* x[6]))


(5) -> (7), if ((ys[5] →* ins(y[7], zs[7]))∧(x[5] →* x[7]))


(6) -> (1), if ((zs[6] →* zs[1])∧(x[6] →* x[1])∧(y[6] →* y[1])∧(min(y[6], zs[6]) →* pair(m[1], zh[1])))


(7) -> (4), if ((zs[7] →* ins(y[4], zs[4]))∧(y[7] →* x[4]))


(7) -> (6), if ((zs[7] →* ins(y[6], zs[6]))∧(y[7] →* x[6]))


(7) -> (7), if ((zs[7] →* ins(y[7]a, zs[7]a))∧(y[7] →* x[7]a))



The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 5 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph contains the following rules and edges:

(7): MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

(7) -> (7), if ((zs[7] →* ins(y[7]a, zs[7]a))∧(y[7] →* x[7]a))



The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph contains the following rules and edges:

(7): MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

(7) -> (7), if ((zs[7] →* ins(y[7]a, zs[7]a))∧(y[7] →* x[7]a))



The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(MIN(x1, x2)) = -1 + x2   
POL(ins(x1, x2)) = 1 + x2   
POL(TRUE) = 0   
POL(FALSE) = 0   
POL(undefined) = 0   

The following pairs are in P>:

MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

The following pairs are in Pbound:

MIN(x[7], ins(y[7], zs[7])) → MIN(y[7], zs[7])

The following pairs are in P≥:
none

There are no usable rules.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph contains the following rules and edges:

(2): MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])
(3): IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3])

(2) -> (3), if ((x[2] →* x[3])∧(ys[2] →* ys[3])∧(min(x[2], ys[2]) →* pair(m[3], zs[3])))


(3) -> (2), if ((zs[3] →* ins(x[2], ys[2])))



The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2]) the following chains were created:




For Pair IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(ins(x1, x2)) = 1 + x2   
POL(e) = 0   
POL(TRUE) = 0   
POL(Cond_if_2(x1, x2, x3, x4, x5, x6)) = 2 + x3   
POL(IF_3(x1, x2, x3)) = 2 + x1   
POL(MSORT(x1)) = 2 + x1   
POL(if_1(x1, x2, x3, x4)) = 1 + x1   
POL(FALSE) = 0   
POL(if_2(x1, x2, x3, x4)) = 1 + x1   
POL(>@z(x1, x2)) = 0   
POL(Cond_if_1(x1, x2, x3, x4, x5, x6)) = 2 + x3   
POL(>=@z(x1, x2)) = 0   
POL(pair(x1, x2)) = 1 + x2   
POL(min(x1, x2)) = 1 + x2   
POL(undefined) = 0   

The following pairs are in P>:

IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3])

The following pairs are in Pbound:

MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])
IF_3(pair(m[3], zs[3]), x[3], ys[3]) → MSORT(zs[3])

The following pairs are in P≥:

MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

min(x, ins(y, zs))1 ↔ if_1(min(y, zs), x, y, zs)1
min(x, ins(y, zs))1 ↔ if_2(min(y, zs), x, y, zs)1
if_1(pair(m, zh), x, y, zs)1 ↔ Cond_if_1(>@z(m, x), m, zh, x, y, zs)1
Cond_if_1(TRUE, m, zh, x, y, zs)1 ↔ pair(x, ins(m, zh))1
min(x, e)1 ↔ pair(x, e)1
Cond_if_2(TRUE, m, zh, x, y, zs)1 ↔ pair(m, ins(x, zh))1
if_2(pair(m, zh), x, y, zs)1 ↔ Cond_if_2(>=@z(x, m), m, zh, x, y, zs)1


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                      ↳ IDependencyGraphProof
                    ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph is empty.
The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ IDPNonInfProof
                  ↳ AND
                    ↳ IDP
                    ↳ IDP
                      ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(x, ins(y, zs)) → if_1(min(y, zs), x, y, zs)
min(x, ins(y, zs)) → if_2(min(y, zs), x, y, zs)
if_1(pair(m, zh), x, y, zs) → Cond_if_1(>@z(m, x), m, zh, x, y, zs)
Cond_if_1(TRUE, m, zh, x, y, zs) → pair(x, ins(m, zh))
min(x, e) → pair(x, e)
Cond_if_2(TRUE, m, zh, x, y, zs) → pair(m, ins(x, zh))
if_2(pair(m, zh), x, y, zs) → Cond_if_2(>=@z(x, m), m, zh, x, y, zs)

The integer pair graph contains the following rules and edges:

(2): MSORT(ins(x[2], ys[2])) → IF_3(min(x[2], ys[2]), x[2], ys[2])


The set Q consists of the following terms:

min(x0, ins(x1, x2))
msort(e)
if_1(pair(x0, x1), x2, x3, x4)
Cond_if_1(TRUE, x0, x1, x2, x3, x4)
msort(ins(x0, x1))
if_3(pair(x0, x1), x2, x3)
min(x0, e)
Cond_if_2(TRUE, x0, x1, x2, x3, x4)
if_2(pair(x0, x1), x2, x3, x4)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.